A:Type, eq:EqDecider(A), B:Top, f:a:A fp Top.  || f 

latex

Definitions	a:A fp B(a), EqDecider(T), f || g, P  Q, x(s), P & Q, Prop, Top, x. t(x), x:A. B(x), t  T, , x  dom(f), b, False
Lemmas	fpf-dom wf, assert wf, fpf-empty wf, deq wf, top wf, fpf wf